f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
↳ QTRS
↳ DependencyPairsProof
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
Used ordering: Polynomial interpretation [21]:
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
POL(F2(x1, x2)) = x1
POL(a) = 1
POL(b) = 1
POL(c) = 0
POL(f2(x1, x2)) = x1
f2(x, f2(y, z)) -> f2(f2(x, y), z)
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(f2(a, b), x) -> F2(a, x)
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(b, f2(a, x))
Used ordering: Polynomial interpretation [21]:
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(f2(a, b), x) -> F2(a, x)
F2(x, f2(y, z)) -> F2(f2(x, y), z)
POL(F2(x1, x2)) = x1
POL(a) = 3
POL(b) = 0
POL(c) = 0
POL(f2(x1, x2)) = x1
f2(x, f2(y, z)) -> f2(f2(x, y), z)
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)